package kodkod.analysis.ordering;

import java.text.DecimalFormat;
import java.text.DecimalFormatSymbols;
import java.text.NumberFormat;

import kodkod.analysis.Analyzer;
import kodkod.analysis.OrderableSolver;
import kodkod.ast.Relation;
import kodkod.engine.fol2sat.Translation;

public class SoloPromotion extends AbstractOrdering {
	
	public Analyzer analyzer = null;
	public double weight = 0.0;
	
	public SoloPromotion() {
		this(null);
	}
	
	public SoloPromotion(Analyzer analyzer) {
		this(analyzer, 1.0);
	}
	
	public SoloPromotion(Analyzer analyzer, double weight) {
		super();
		this.analyzer = analyzer;
		this.weight = weight;
	}
	
	public void apply(Translation translation) {
		if (analyzer == null) {
			analyzer = new Analyzer(translation);
		}
		int index = analyzer.getRelationIdsOrdered().get(0);
		System.out.println("Promoting Relation " + index);

		Relation rel = translation.primaryRelations.get(index);
		int[] vars = translation.primaryVariables(rel).toArray();
		for (int var : vars) {
			weightVariable((OrderableSolver)translation.cnf(), var, weight);
		}
	}
	
	public String toString() {
		StringBuffer buf = new StringBuffer();
		if (softOrder) {
			buf.append("SoloInitialize");
			DecimalFormatSymbols symbols = new DecimalFormatSymbols();
			symbols.setDecimalSeparator('.');
			NumberFormat format = new DecimalFormat("#0.00", symbols);
			buf.append("(");
			buf.append(format.format(weight));
			buf.append(")");
		} else {
			buf.append("SoloOverride");
		}
		return buf.toString();
	}
}
